Nuprl Lemma : aframe-p_wf
0,22
postcript
pdf
es
:ES,
i
:Id,
k
:Knd,
L
:Id List. @
i
:
k
affects only
L
Prop
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
vartype(
i
;
x
)
,
{
T
}
,
P
Q
,
SQType(
T
)
,
Id
,
s
=
t
,
Prop
,
s
~
t
,
x
:
A
B
(
x
)
,
Knd
,
left
+
right
,
ES
,
Type
,
type
List
,
loc(
e
)
,
E
,
{
x
:
A
|
B
(
x
) }
,
x
:
A
B
(
x
)
,
f
(
a
)
,
x
when
e
,
(
x
after
e
)
,
(
x
l
)
,
A
,
P
&
Q
,
kind(
e
)
,
x
.
t
(
x
)
,
e
@
i
.
P
(
e
)
,
@
i
:
k
affects only
L
Lemmas
alle-at
wf
,
es-kind
wf
,
not
wf
,
l
member
wf
,
es-after
wf
,
es-when
wf
,
es-E
wf
,
es-loc
wf
,
event
system
wf
,
Knd
wf
,
Knd
sq
,
Id
wf
,
Id
sq
,
subtype
rel
self
,
es-vartype
wf
origin
es:ES, i:Id, k:Knd, L:Id List. @i: k affects only L 
Prop es:ES, i:Id, k:Knd, L:Id List. @i: k affects only L Prop Tx:A. B(x)
Q
B(x)
B(x) l)
A
x. t(x)e@i. P(e)